i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl(ds; da), snd:msg-spec(ds; da),
upd:update-spec(ds; da).
update-spec-decl(upd; ds)
 ((fpf-dom(id-deq; mkid{ecl:ut2}; ds)))
 (ecl-machine{ecl:ut2}(i; ds; da; A; snd; upd)  es_realizer{i:l}) 

latex

Definitions	x. t(x), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-machine{$ecl:ut2}(i; ds; da; A; snd; upd), t  T, mkid{$x:ut2}, P  Q, Id, x:A. B(x), x(s), ecl-trans-tuple{i:l}(ds; da), prop{i:l}
Lemmas	Knd wf, fpf wf, ecl wf, msg-spec wf, update-spec wf, update-spec-decl wf, fpf-trivial-subtype-top, id-deq wf, Id wf, fpf-dom wf, assert wf, not wf, ecl-machine3 wf, ecl-machine2 wf, ecl-trans-tuple wf, ecl-trans wf, ecl-machine1 wf, Rplus wf